///
/// \file main.cc
/// \brief Implementation of the main function of the program.
/// \author Coddy Levi, Sylvain Lobry
/// \version 1.0
///


#include "Model.hh"

#include "basic_set_operations.hh"
#include "CTLLexer.hh"
#include "CTLParser.hh"
#include "eval.hh"

#include <fstream>
#include <iostream>
#include <sstream>
#include <bdd.h>


///
/// \fn int main (int argc, char* argv[])
/// \brief Main function.
///
/// \param[in]	argc the number of arguments.
/// \param[in]	argv the arguments.
///
/// \return	The exit code.
///
int main(int argc, char* argv[])
{
  int size;

  std::ifstream ifs(argv[1]);

  //Retrive the size to init the bdd.
  size = Model::parse_size(ifs);

  //Initialisation of the bdd.
  bdd_init(size, size > 10 ? size / 10 : size);

  //Retrieve the number of variables in the structure.
  int nb_variables = Model::compute_nb_variables(size);
  bdd_setvarnum(nb_variables * 2);

  //Initialisation of the model representing the kripke structure.
  Model model;

  model.set_nb_state_variables(nb_variables);
  model.parse_model(ifs);

  std::istream* formulae_stream;

  if (argc == 3)
    {
      formulae_stream = new std::istringstream(argv[2]);
    }
  else
    {
      formulae_stream = &std::cin;
    }

  while (formulae_stream->good())
    {
      std::string formula;
      
      getline(*formulae_stream, formula);

      if (formula.size() == 0)
	break;

      //Initialisation of the lexer.
      CTLLexer lex = CTLLexer(formula);
      //Construction of the AST.
      AST* formula_ast = parseCTL(lex);

      //Evaluation.
      bdd states = eval(formula_ast, model);

      //print the result.
      if ((states & model.make_state(0)) != bddfalse)
	std::clog << "true" << std::endl;
      else
	std::clog << "false" << std::endl;
    }

  if (argc == 3)
    {
      delete formulae_stream;
    }

  //Unallocate the bdd.
  bdd_done();

  return 0;
}
